ds:x:Id fp Type, da:k:Knd fp Type, a, b:update-spec(ds;da). a  b  update-spec(ds;da) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, x:AB(x), Void, x.A(x), 2of(t), IdDeq, f(x)?z, 1of(t), Valtype(da;k), x:AB(x), State(ds), , type List, KindDeq, product-deq(A;B;a;b), f  g, a  b, update-spec(ds;da)
Lemmas	fpf-join wf, product-deq wf, Kind-deq wf, nat wf, decl-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, fpf wf, Id wf